Nuprl Definition : es-x-equiv 0,22

s1  s2 mod x@i == z:Id. z = x  s1(z) = s2(z) 
latex



clarification:

es-x-equiv(es;i;x;s1;s2) == z:Id. z = x  Id  s1(z) = s2(z)  es-vartype(es; i; z) 
latex


Definitionsx:A. B(x), P  Q, A, Id, s = t, vartype(i;x), f(a)
FDL editor aliaseses-x-equiv

origin